(set-logic ALL)
(set-info :status unsat)
(declare-sort $$unsorted 0)
(declare-fun tptp.cEUCountry ($$unsorted) Bool)
(assert (forall ((A $$unsorted) (B $$unsorted)) (=> (and (= A B) (tptp.cEUCountry A)) (tptp.cEUCountry B))))
(declare-fun tptp.cEuroMP ($$unsorted) Bool)
(assert (forall ((A $$unsorted) (B $$unsorted)) (=> (and (= A B) (tptp.cEuroMP A)) (tptp.cEuroMP B))))
(declare-fun tptp.cEuropeanCountry ($$unsorted) Bool)
(assert (forall ((A $$unsorted) (B $$unsorted)) (=> (and (= A B) (tptp.cEuropeanCountry A)) (tptp.cEuropeanCountry B))))
(declare-fun tptp.cPerson ($$unsorted) Bool)
(assert (forall ((A $$unsorted) (B $$unsorted)) (=> (and (= A B) (tptp.cPerson A)) (tptp.cPerson B))))
(declare-fun tptp.cowlNothing ($$unsorted) Bool)
(assert (forall ((A $$unsorted) (B $$unsorted)) (=> (and (= A B) (tptp.cowlNothing A)) (tptp.cowlNothing B))))
(declare-fun tptp.cowlThing ($$unsorted) Bool)
(assert (forall ((A $$unsorted) (B $$unsorted)) (=> (and (= A B) (tptp.cowlThing A)) (tptp.cowlThing B))))
(declare-fun tptp.rhasEuroMP ($$unsorted $$unsorted) Bool)
(assert (forall ((A $$unsorted) (B $$unsorted) (C $$unsorted)) (=> (and (= A B) (tptp.rhasEuroMP A C)) (tptp.rhasEuroMP B C))))
(assert (forall ((A $$unsorted) (B $$unsorted) (C $$unsorted)) (=> (and (= A B) (tptp.rhasEuroMP C A)) (tptp.rhasEuroMP C B))))
(declare-fun tptp.risEuroMPFrom ($$unsorted $$unsorted) Bool)
(assert (forall ((A $$unsorted) (B $$unsorted) (C $$unsorted)) (=> (and (= A B) (tptp.risEuroMPFrom A C)) (tptp.risEuroMPFrom B C))))
(assert (forall ((A $$unsorted) (B $$unsorted) (C $$unsorted)) (=> (and (= A B) (tptp.risEuroMPFrom C A)) (tptp.risEuroMPFrom C B))))
(declare-fun tptp.xsd_integer ($$unsorted) Bool)
(assert (forall ((A $$unsorted) (B $$unsorted)) (=> (and (= A B) (tptp.xsd_integer A)) (tptp.xsd_integer B))))
(declare-fun tptp.xsd_string ($$unsorted) Bool)
(assert (forall ((A $$unsorted) (B $$unsorted)) (=> (and (= A B) (tptp.xsd_string A)) (tptp.xsd_string B))))
(assert (forall ((X $$unsorted)) (and (tptp.cowlThing X) (not (tptp.cowlNothing X)))))
(assert (forall ((X $$unsorted)) (= (tptp.xsd_string X) (not (tptp.xsd_integer X)))))
(declare-fun tptp.iPT () $$unsorted)
(declare-fun tptp.iBE () $$unsorted)
(declare-fun tptp.iNL () $$unsorted)
(declare-fun tptp.iES () $$unsorted)
(declare-fun tptp.iFR () $$unsorted)
(declare-fun tptp.iUK () $$unsorted)
(assert (forall ((X $$unsorted)) (= (tptp.cEUCountry X) (or (= X tptp.iPT) (= X tptp.iBE) (= X tptp.iNL) (= X tptp.iES) (= X tptp.iFR) (= X tptp.iUK)))))
(assert (forall ((X $$unsorted)) (= (tptp.cEuroMP X) (exists ((Y $$unsorted)) (and (tptp.risEuroMPFrom X Y) (tptp.cowlThing Y))))))
(assert (forall ((X $$unsorted) (Y $$unsorted)) (=> (tptp.rhasEuroMP X Y) (tptp.cEUCountry X))))
(assert (forall ((X $$unsorted) (Y $$unsorted)) (= (tptp.risEuroMPFrom X Y) (tptp.rhasEuroMP Y X))))
(assert (tptp.cEuropeanCountry tptp.iBE))
(assert (tptp.cEuropeanCountry tptp.iES))
(assert (tptp.cEuropeanCountry tptp.iFR))
(declare-fun tptp.iKinnock () $$unsorted)
(assert (tptp.cPerson tptp.iKinnock))
(assert (not (tptp.cEuroMP tptp.iKinnock)))
(assert (tptp.cEuropeanCountry tptp.iNL))
(assert (tptp.cEuropeanCountry tptp.iPT))
(assert (tptp.cEuropeanCountry tptp.iUK))
(assert (tptp.rhasEuroMP tptp.iUK tptp.iKinnock))
(set-info :filename KRS063+1)
(check-sat)
